/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979
␈↓ ↓H␈↓␈↓ ¬DPROBLEM SET  1
␈↓ ↓H␈↓␈↓ ¬uDue  Oct. 12

␈↓ ↓H␈↓1.␈αWrite␈αa␈α
program␈αto␈αcompute␈α␈↓↓commontail[u,v],␈↓␈α
 the␈αlongest␈αcommon␈αsublist␈α
of␈α␈↓↓u␈↓␈αand␈α
␈↓↓v␈↓␈αending
␈↓ ↓H␈↓␈↓ ↓xwith the ends of the lists.  Thus

␈↓ ↓H␈↓␈↓ ∧β␈↓↓commontail[␈↓¬(A B C D E),(A C D E)␈↓↓] = ␈↓¬(C D E)␈↓↓␈↓. 

␈↓ ↓H␈↓2.␈αWrite␈α
a␈αprogram␈α to␈α
compute␈α␈↓↓mapleaf[f,x],␈↓␈αthe␈α
list␈αof␈αexpressions␈α
␈↓↓f a␈↓␈αsuch␈αthat␈α
␈↓↓a␈↓␈αis␈α
an␈αatom
␈↓ ↓H␈↓␈↓ ↓xoccuring␈α∞in␈α∞␈↓↓x,␈↓␈α∞appearing␈α∞in␈α
the␈α∞same␈α∞order␈α∞as␈α∞the␈α
atoms␈α∞appear␈α∞in␈α∞the␈α∞printed␈α
expression.
␈↓ ↓H␈↓␈↓ ↓xThus

␈↓ ↓H␈↓␈↓ βo␈↓↓mapleaf[λz.<z>, ␈↓¬((A . B) . C)␈↓↓] = ␈↓¬((A) (B) (C))␈↓↓␈↓ 

␈↓ ↓H␈↓[Note that ␈↓↓mapleaf[λz.z,x]=fringe x␈↓]

␈↓ ↓H␈↓3.  Consider arithmetic expressions as represented in Chapters I and II.  Namely an expression is

␈↓ ↓H␈↓␈↓ αH        (i) a number (satisfies ␈↓↓numberp),␈↓
␈↓ ↓H␈↓␈↓ αH        (ii) a variable (not a number and satisfies ␈↓αat␈↓),
␈↓ ↓H␈↓␈↓ αH        (iii) a sum : ␈↓¬PLUS ␈↓. < list of expressions > or
␈↓ ↓H␈↓␈↓ αH        (iv) a product : ␈↓¬TIMES ␈↓. < list of expressions >.

␈↓ ↓H␈↓    (For simplicity, assume the sum and product lists always have at least 2 elements.)

␈↓ ↓H␈↓        The␈α∂function␈α∂␈↓↓sop␈↓␈α∂converts␈α∂such␈α∂expressions␈α∂into␈α∂sum␈α∂of␈α∂products␈α∂form,␈α∂eg.␈α⊂the␈α∂resulting
␈↓ ↓H␈↓␈↓ ↓xexpression␈α↔is␈α↔either␈α↔a␈α↔monomial␈α↔or␈α↔a␈α↔sum␈α↔of␈α↔monomial␈α↔terms␈α↔which␈α↔has␈α↔the␈α⊗form
␈↓ ↓H␈↓␈↓ ↓x␈↓¬PLUS␈↓ . <list of monomials>.␈α
 A␈α
monomial␈α∞is␈α
either␈α
a␈α∞number,␈α
a␈α
variable,␈α∞or␈α
a␈α
product␈α∞of␈α
the
␈↓ ↓H␈↓␈↓ ↓xform ␈↓¬TIMES␈↓ . < list of numbers or variables >.

␈↓ ↓H␈↓␈↓ αH␈↓↓sop ␈↓¬(TIMES (PLUS X 1) (PLUS  Y Z) 3)␈↓↓=␈↓
␈↓ ↓H␈↓␈↓ αH      ␈↓¬(PLUS (TIMES X Y 3) (TIMES X Z 3) (TIMES 1 Y 3) (TIMES 1 Z 3))␈↓

␈↓ ↓H␈↓        Write␈α⊂a␈α∂program␈α⊂to␈α∂comute␈α⊂␈↓↓sop.␈↓␈α⊂ Try␈α∂it␈α⊂on␈α∂expressions␈α⊂returned␈α∂by␈α⊂␈↓↓diff.␈↓␈α⊂ What␈α∂about
␈↓ ↓H␈↓␈↓ ↓x␈↓↓diff[sop e,v]␈↓␈α∃and␈α∀␈↓↓sop diff[sop e,v]␈↓?␈α∃ Consider␈α∃how␈α∀you␈α∃might␈α∃convince␈α∀a␈α∃user␈α∃of␈α∀your
␈↓ ↓H␈↓␈↓ ↓xprogram that ␈↓↓numval[e,alist]=numval[sop e,alist]␈↓.  (␈↓↓numval␈↓ is defined on page 38.)

␈↓ ↓H␈↓4.␈α Consider␈αan␈αalternate␈αrepresentation␈αof␈αgraphs␈αby␈αlists␈αin␈αwhich␈αa␈αgraph␈αis␈αa␈αlist␈αof␈αedges␈αand
␈↓ ↓H␈↓␈↓ ↓xan edge is a list of the form

␈↓ ↓H␈↓␈↓ βq␈↓↓␈↓¬(<source vertex> <target vertex> . <data>)␈↓↓.␈↓ 

␈↓ ↓H␈↓and␈α
 represents␈α
an␈α
edge␈αof␈α
the␈α
graph␈α
from␈αthe␈α
␈↓¬<source vertex>␈α
␈↓to␈α
the␈α
␈↓¬<target vertex>.␈αIn
␈↓ ↓H␈↓¬␈↓ ↓x␈↓the case of the simple unlabeled graphs described in Chapter I, the ␈↓¬<data> ␈↓is just ␈↓¬NIL␈↓.

␈↓ ↓H␈↓4.1.␈α∂Write␈α⊂programs␈α∂␈↓↓mk-edge-rep[g]␈↓␈α⊂and␈α∂␈↓↓mk-neigh-rep[g]␈↓␈α⊂that␈α∂convert␈α⊂a␈α∂representation␈α⊂ of␈α∂a
␈↓ ↓H␈↓␈↓ ↓xgraph␈α
as␈α
a␈α
list␈α
of␈α
neighbors␈α
(a␈α
la␈α
Chpater␈αI.)␈α
to␈α
a␈α
representation␈α
as␈α
a␈α
list␈α
of␈α
edges,␈α
and␈αvice
␈↓ ↓H␈↓␈↓ ↓xversa.  Thus
␈↓ ↓H␈↓2␈↓ H



␈↓ ↓H␈↓␈↓ αH␈↓↓mk-edge-rep[␈↓¬((A B)(B A C D)(C D B)(D B C))␈↓↓]=␈↓
␈↓ ↓H␈↓␈↓ αH           ␈↓¬((A B)(B A)(B C)(B D)(C D)(C B)(D B)(D C))␈↓

␈↓ ↓H␈↓␈↓ αH␈↓↓mk-neigh-rep[␈↓¬((A B)(B A)(B C)(B D)(C D)(C B)(D B)(D C))␈↓↓]=␈↓
␈↓ ↓H␈↓␈↓ αH           ␈↓¬((A B)(B A C D)(C D B)(D B C))␈↓

␈↓ ↓H␈↓        A␈α
current␈α∞graph␈α
is␈α∞a␈α
directed␈α∞graph␈α
with␈α
edges␈α∞labeled␈α
by␈α∞numbers␈α
corresponding␈α∞to␈α
the
␈↓ ↓H␈↓␈↓ ↓x"current"␈αflowing␈α
into␈αthe␈αtarget␈α
vertex␈αalong␈α
that␈αedge.␈α A␈α
current␈αgraph␈α
satisfies␈αKirchoff's
␈↓ ↓H␈↓␈↓ ↓xlaw␈αif␈αfor␈αeach␈αvertex,␈αthe␈αsum␈α of␈αthe␈αcurrents␈αflowing␈αin␈αis␈αequal␈αto␈αthe␈αsum␈αof␈αthe␈αcurrents
␈↓ ↓H␈↓␈↓ ↓xflowing out.

␈↓ ↓H␈↓4.2.␈α
 Write␈α
a␈α
program␈α
␈↓↓Kirch[g]␈↓␈αthat␈α
returns␈α
␈↓¬T␈↓␈α
if␈α
␈↓↓g␈↓␈α
is␈αa␈α
current␈α
graph␈α
satisfying␈α
Kirchoff's␈αlaw,␈α
and
␈↓ ↓H␈↓␈↓ ↓x␈↓¬NIL␈↓ otherwise.   Thus

␈↓ ↓H␈↓␈↓ β=␈↓↓Kirch[␈↓¬((A B 1) (A D 1) (B C 1) (C A 2) (D C 1))␈↓↓] =␈↓¬T␈↓↓␈↓ 

␈↓ ↓H␈↓␈↓ ∧-␈↓↓Kirch[␈↓¬((A D 1) (B D 1) (D C 2))␈↓↓] =␈↓¬NIL␈↓↓␈↓ 


␈↓ ↓H␈↓αContinuing problem.

␈↓ ↓H␈↓5.␈α
This␈αproblem␈α
deals␈α
with␈αrepresentation␈α
and␈αmanipulation␈α
of␈α
expressions␈αin␈α
the␈αpure␈α
λ-calculus.
␈↓ ↓H␈↓␈↓ ↓xThe␈α
basic␈αproperties␈α
and␈αmanipulations␈α
of␈α␈↓¬LAMB␈↓-expressions␈α
are␈αdefined␈α
and␈αyou␈α
are␈αasked␈α
to
␈↓ ↓H␈↓␈↓ ↓xwrite␈αthe␈αcorresponding␈αprograms.␈α The␈αgoal␈αis␈αa␈αprogram␈αthat␈αwill␈αapply␈αa␈αlist␈αof␈αreductions
␈↓ ↓H␈↓␈↓ ↓xto an expression.

␈↓ ↓H␈↓        The␈α∂simplest␈α∞λ-expression␈α∂is␈α∞a␈α∂variable,␈α∞represented␈α∂by␈α∞a␈α∂␈↓¬LAMB␈↓-variable␈α∞which␈α∂is␈α∂a␈α∞pair
␈↓ ↓H␈↓␈↓ ↓x␈↓¬(X . n)␈↓,␈α⊃␈↓¬n=0, 1, 2, ...␈↓.␈α⊃ The␈α⊃class,␈α⊃␈↓¬LAMB␈↓-expressions,␈α⊃of␈α⊃S-expressions␈α⊃representing␈α⊃λ-
␈↓ ↓H␈↓␈↓ ↓xexpressions is defined inductively as follows:

␈↓ ↓H␈↓␈↓ αλ  (i) a ␈↓¬LAMB␈↓-variable is a ␈↓¬LAMB␈↓-expression (of sort variable),
␈↓ ↓H␈↓␈↓ αλ (ii)␈α∂if␈α∂␈↓↓e1␈↓␈α∂and␈α∂ ␈↓↓e2␈↓␈α∂are␈α∂␈↓¬LAMB␈↓-expressions␈α∂then␈α∂␈↓¬(APPL␈α∂e1␈α∂e1)␈↓␈α∂is␈α∂a␈α∂␈↓¬LAMB␈↓-expression␈α⊂(of␈α∂sort
␈↓ ↓H␈↓␈↓ αHapplication),
␈↓ ↓H␈↓␈↓ αλ(iii)␈α∞if␈α∞␈↓↓e␈↓␈α∂is␈α∞a␈α∞␈↓¬LAMB␈↓-expression␈α∞then␈α∂for␈α∞each␈α∞␈↓↓n,␈↓␈α∞␈↓¬(LAMB n e)␈↓␈α∂is␈α∞a␈α∞␈↓¬LAMB␈↓-expression␈α∂(of␈α∞sort
␈↓ ↓H␈↓␈↓ αHabstraction), representing abstraction with respect to the ␈↓↓n␈↓th variable ␈↓¬(X . n)␈↓.
␈↓ ↓H␈↓␈↓ αλ (iv) These are all of the ␈↓¬LAMB␈↓-expressions.

␈↓ ↓H␈↓5.1. Write a program ␈↓↓islamb[e]␈↓ which returns ␈↓¬T␈↓ if ␈↓↓e␈↓ is a ␈↓¬LAMB␈↓-expression and ␈↓¬NIL␈↓ otherwise.

␈↓ ↓H␈↓[Remark:␈α⊃ you␈α⊃will␈α⊃find␈α⊃programs␈α⊃computing␈α⊂the␈α⊃predicates␈α⊃␈↓↓var,␈↓␈α⊃␈↓↓appl,␈↓␈α⊃and␈α⊃␈↓↓abstr␈↓␈α⊃which␈α⊂are
␈↓ ↓H␈↓␈↓ ↓xsatisfied by the three types of ␈↓¬LAMB␈↓-expressions useful, here and later.]

␈↓ ↓H␈↓        In␈αthe␈αfollowing␈αwe␈αwill␈αuse␈αvariable␈αto␈αmean␈α␈↓¬LAMB␈↓-variable␈αand␈αexpression␈αto␈αmean␈α␈↓¬LAMB␈↓-
␈↓ ↓H␈↓␈↓ ↓xexpression.

␈↓ ↓H␈↓        An␈αoccurrence␈αof␈αa␈αvariable,␈α
␈↓↓v,␈↓␈αin␈αan␈αexpression␈α␈↓↓e,␈↓␈α can␈α
be␈αclassified␈αas␈αfree␈αor␈α
bound␈αas
␈↓ ↓H␈↓␈↓ ↓xfollows.␈α
 If␈α␈↓↓e␈↓␈α
is␈αthe␈α
variable␈α
␈↓↓v,␈↓␈αthen␈α
the␈αoccurrence␈α
of␈α
␈↓↓v␈↓␈αin␈α
␈↓↓e␈↓␈αis␈α
free␈α
in␈α␈↓↓e.␈↓␈α
 If␈α␈↓↓e␈↓␈α
is␈αan␈α
abstraction
␈↓ ↓H␈↓␈↓ ↓xon␈α␈↓↓v,␈↓␈αe.g.␈α␈↓↓e␈↓␈αis␈αof␈αthe␈αform␈α␈↓¬(LAMB n e1)␈↓␈αand␈α
␈↓↓v␈↓␈αis␈α␈↓¬(X . n)␈↓␈αthen␈αa␈αfree␈αoccurrence␈αof␈α␈↓↓v␈↓␈αin␈α␈↓↓e1␈↓␈α
is
␈↓ ↓H␈↓␈↓ ↓xbound␈α⊂by␈α⊂this␈α⊂␈↓¬LAMB␈↓.␈α∂ If␈α⊂␈↓↓e␈↓␈α⊂is␈α⊂of␈α∂the␈α⊂form␈α⊂␈↓¬(LAMB n e1)␈↓,␈α⊂where␈α∂␈↓↓v␈↓␈α⊂is␈α⊂not␈α⊂␈↓¬(X . N)␈↓,␈α⊂then␈α∂an
␈↓ ↓H␈↓␈↓ 93


␈↓ ↓H␈↓␈↓ ↓xoccurrence␈α
of␈α
␈↓↓v␈↓␈α
(in␈α
␈↓↓e1␈↓)␈α
is␈α
bound␈α
or␈α
free␈α
in␈α
␈↓↓e␈↓␈α
according␈α
as␈α
it␈α
is␈α
bound␈α
or␈α
free␈α
in␈α
␈↓↓e1␈↓.␈α Similarly,␈α
if
␈↓ ↓H␈↓␈↓ ↓x␈↓↓e␈↓␈α
is␈α∞of␈α
the␈α
form␈α∞␈↓¬(APPL e1 e2)␈↓,␈α
an␈α
occurrence␈α∞of␈α
␈↓↓v␈↓␈α
in␈α∞in␈α
␈↓↓e1␈↓␈α
(resp.␈α∞␈↓↓e2␈↓)␈α
is␈α
bound␈α∞or␈α
free␈α∞in␈α
␈↓↓e␈↓
␈↓ ↓H␈↓␈↓ ↓xaccording as it is bound or free in ␈↓↓e1␈↓ (resp. ␈↓↓e2␈↓).

␈↓ ↓H␈↓        An␈αoccurrence␈αof␈α␈↓↓v␈↓␈αin␈α␈↓↓e␈↓␈αis␈αdesignated␈α
by␈αthe␈αlist␈αof␈α"moves",␈αcalled␈αa␈α␈↓↓location,␈↓␈α
necessary␈αto
␈↓ ↓H␈↓␈↓ ↓xget␈αfrom␈α␈↓↓e␈↓␈αto␈αthe␈αsubexpression␈αof␈α␈↓↓e␈↓␈αwhich␈αis␈α
the␈αoccurrence␈αof␈α␈↓↓v.␈↓␈α   If␈α␈↓↓e␈↓␈αis␈α␈↓↓v␈↓␈αthen␈αthe␈α
location
␈↓ ↓H␈↓␈↓ ↓xis␈α∞the␈α∞empty␈α∞list.␈α∞ If␈α∞␈↓↓e␈↓␈α
is␈α∞␈↓¬(APPL␈α∞e1␈α∞e2)␈↓␈α∞and␈α∞the␈α∞occurrence␈α
is␈α∞in␈α∞␈↓¬e1␈α∞␈↓then␈α∞the␈α∞location␈α∞is␈α
␈↓¬A1
␈↓ ↓H␈↓¬␈↓ ↓x␈↓followed␈αby␈αthe␈αlist␈αof␈αmoves␈αlocating␈α␈↓¬v␈α␈↓in␈α␈↓¬e1.␈α␈↓␈α(similarly␈αif␈αthe␈αoccurrence␈αis␈αin␈α␈↓¬e2,␈α␈↓with␈α␈↓¬A2
␈↓ ↓H␈↓¬␈↓ ↓x␈↓instead␈α⊃of␈α⊂␈↓¬A1␈↓.)␈α⊃If␈α⊂␈↓↓e␈↓␈α⊃is␈α⊃␈↓¬(LAMB␈α⊂m␈α⊃e1)␈↓␈α⊂then␈α⊃the␈α⊂location␈α⊃is␈α⊃␈↓¬B␈α⊂␈↓followed␈α⊃by␈α⊂the␈α⊃list␈α⊃of␈α⊂moves
␈↓ ↓H␈↓␈↓ ↓xlocating ␈↓¬v ␈↓in ␈↓¬e1. ␈↓

␈↓ ↓H␈↓5.2.␈α
 Write␈α
a␈α
program␈α
␈↓↓freeoccs[n,e]␈↓␈α
that␈α
returns␈α
a␈α
list␈α
of␈α
locations␈α
of␈α
free␈α
occurrences␈α
of␈α
the␈α␈↓↓n␈↓th
␈↓ ↓H␈↓␈↓ ↓xvariable, ␈↓¬(X . n)␈↓, in the expression ␈↓↓e.␈↓  (You may assume ␈↓↓e␈↓ to be a ␈↓¬LAMB␈↓-expression.)   Thus

␈↓ ↓H␈↓␈↓ ↓I␈↓↓freeoccs[␈↓¬1␈↓↓,␈↓¬(APPL (LAMB 2 (APPL (X.2) (X.2))) (APPL (X.1) (X.1)))␈↓↓]= ␈↓¬((A2 A1)(A2 A2))␈↓↓␈↓ 

␈↓ ↓H␈↓5.3. Write a program ␈↓↓substfree[e1,n,e]␈↓ which substitutes ␈↓↓e1␈↓ for free occurrences of ␈↓¬(X . n)␈↓ in ␈↓↓e.␈↓

␈↓ ↓H␈↓        Note␈α∂that␈α∂we␈α∂haven't␈α∂provided␈α∂a␈α∂means␈α∂to␈α∂prevent␈α∂trapping␈α∂of␈α∂free␈α∂variables␈α∂of␈α∂␈↓↓e1.␈↓␈α∞ If
␈↓ ↓H␈↓␈↓ ↓x␈↓¬(X . m)␈↓␈α
occurrs␈α
free␈α
in␈α
␈↓↓e1␈↓␈αand␈α
␈↓↓v␈↓␈α
occurs␈α
free␈α
in␈α
a␈αsubexpression␈α
of␈α
␈↓↓e␈↓␈α
of␈α
the␈αform␈α
␈↓¬(LAMB m e2)␈↓
␈↓ ↓H␈↓␈↓ ↓xthe␈αoccurrence␈αof␈α␈↓¬(X . m)␈↓␈αin␈α␈↓↓e1␈↓␈αwill␈αbe␈α
"trapped"␈αupon␈αsubstitution.␈α That␈αis␈αit␈αwill␈αbe␈α
bound
␈↓ ↓H␈↓␈↓ ↓xin␈αthe␈αresulting␈αexpression.␈α This␈αcauses␈αundesired␈αbehaviour␈αin␈αthe␈αλ-calculus,␈αso␈αwe␈αwish␈αto
␈↓ ↓H␈↓␈↓ ↓xprevent such substitutions from occuring.

␈↓ ↓H␈↓5.4.␈αWrite␈αa␈αprogram␈α␈↓↓freefor[e1,n,e]␈↓␈αwhich␈αreturns␈α␈↓¬T␈↓␈αif␈αno␈αfree␈αvariable␈αof␈α␈↓↓e1␈↓␈αwill␈αbecome␈αbound
␈↓ ↓H␈↓␈↓ ↓xupon substitution of ␈↓↓e1␈↓ for each free occurrence of ␈↓¬(X . n)␈↓ in ␈↓↓e.␈↓

␈↓ ↓H␈↓        Since␈αwe␈αdon't␈αwant␈αto␈αbe␈αstuck␈αjust␈αbecause␈αsome␈αexpression␈αis␈αnot␈α"freefor"␈αwe␈αprovide␈αa
␈↓ ↓H␈↓␈↓ ↓xmeans␈α∞of␈α∞modifying␈α∞the␈α∞expression␈α∞␈↓↓e␈↓␈α
so␈α∞that␈α∞␈↓↓e1␈↓␈α∞will␈α∞be␈α∞free␈α
for␈α∞␈↓↓v␈↓␈α∞in␈α∞␈↓↓e.␈↓␈α∞  This␈α∞is␈α∞known␈α
as
␈↓ ↓H␈↓␈↓ ↓xrenaming␈α⊃of␈α⊃bound␈α⊃variables.␈α⊃ It␈α⊃is␈α⊃accomplished␈α⊃for␈α⊃a␈α⊃variable␈α⊃␈↓¬(X . n)␈↓,␈α⊃by␈α∩choosing␈α⊃a
␈↓ ↓H␈↓␈↓ ↓xvariable␈α∞␈↓¬(X . m)␈↓␈α∂that␈α∞is␈α∂unused␈α∞so␈α∞far␈α∂and␈α∞replacing␈α∂each␈α∞subexpression␈α∞of␈α∂␈↓↓e␈↓␈α∞of␈α∂the␈α∞form
␈↓ ↓H␈↓␈↓ ↓x␈↓¬(LAMB n e2)␈↓␈α∪by␈α∀␈↓¬(LAMB m e3)␈↓␈α∪␈↓↓e3␈↓␈α∀is␈α∪obtained␈α∪from␈α∀␈↓↓e2␈↓␈α∪by␈α∀replacing␈α∪each␈α∀occurrence␈α∪of
␈↓ ↓H␈↓␈↓ ↓x␈↓¬(X . n)␈↓ in ␈↓↓e2␈↓ bound by this ␈↓¬LAMB ␈↓by ␈↓¬(X . m)␈↓.

␈↓ ↓H␈↓5.5. Write a program ␈↓↓rename[n,m,e]␈↓ that renames ␈↓¬(X . n)␈↓ to ␈↓¬(X . m)␈↓ in ␈↓↓e␈↓ as outlined above.

␈↓ ↓H␈↓        Now␈α
we␈α
have␈α
all␈α
of␈α
the␈αbasic␈α
programs␈α
needed␈α
to␈α
manipulate␈α
␈↓¬LAMB␈↓-expressions,␈α
carry␈αout
␈↓ ↓H␈↓␈↓ ↓xreductions,␈α
look␈α∞for␈α
normal␈α∞forms,␈α
etc.␈α∞ For␈α
example␈α
we␈α∞can␈α
apply␈α∞a␈α
list␈α∞of␈α
reductions␈α∞to␈α
an
␈↓ ↓H␈↓␈↓ ↓xexpression.␈α≤ There␈α≥are␈α≤two␈α≤basic␈α≥reductions.␈α≤ First,␈α≤␈↓¬(ALPHA n m)␈↓␈α≥applied␈α≤to␈α≥␈↓↓e␈↓␈α≤is
␈↓ ↓H␈↓␈↓ ↓x␈↓↓rename[n,m,e]␈↓.␈α It␈αapplies␈αonly␈αif␈α␈↓¬(X . m)␈↓␈αdoes␈αnot␈αoccur␈αin␈α␈↓↓e.␈↓␈α Second,␈α␈↓¬BETA␈α␈↓applies␈αonly␈αto
␈↓ ↓H␈↓␈↓ ↓xexpressions␈α
␈↓↓e␈↓␈α
of␈α
the␈α∞form␈α
␈↓¬(APPL e1 e2)␈↓␈α
where␈α
␈↓↓e1␈↓␈α
is␈α∞an␈α
abstraction␈α
␈↓¬(LAMB n e3)␈↓␈α
and␈α∞␈↓↓e2␈↓␈α
is
␈↓ ↓H␈↓␈↓ ↓xfree␈α∀for␈α∀␈↓¬(X . n)␈↓␈α∀in␈α∀␈↓↓e1.␈↓␈α∀ The␈α∀result␈α∀of␈α∀applying␈α∀␈↓¬BETA␈α∀␈↓to␈α∀␈↓↓e␈↓␈α∀is␈α∀␈↓↓substfree[e2,n,e1]␈↓.␈α∪ We
␈↓ ↓H␈↓␈↓ ↓xgeneralize␈α~these␈α~reductions␈α~to␈α~apply␈α→to␈α~subxexpressions␈α~of␈α~an␈α~expression␈α~␈↓↓e.␈↓␈α→ Thus
␈↓ ↓H␈↓␈↓ ↓x␈↓¬(ALPHA n m loc)␈↓␈α
applied␈α
to␈α
␈↓↓e␈↓␈αis␈α
obtained␈α
by␈α
replacing␈α
the␈αsubexpression␈α
located␈α
at␈α
␈↓↓loc␈↓␈αby␈α
the
␈↓ ↓H␈↓␈↓ ↓xresult␈αof␈αapplying␈α
␈↓¬(ALPHA n m)␈↓␈αto␈αthat␈α
subexpression.␈α It␈αonly␈α
applies␈αif␈α␈↓↓loc␈↓␈α
is␈αa␈αvalid␈α
location
␈↓ ↓H␈↓␈↓ ↓xin ␈↓↓e␈↓ and the ␈↓¬ALPHA ␈↓reduction applies to that subexpression.  Similarly for ␈↓¬(BETA loc)␈↓.

␈↓ ↓H␈↓5.6.␈α
 Write␈α
a␈α
program␈α
␈↓↓LAMB-reduce[e,rlist]␈↓␈α
that␈α
applies␈α
a␈α
list␈α
of␈α
reductions␈α
to␈αa␈α
␈↓¬LAMB␈↓-expression.
␈↓ ↓H␈↓␈↓ ↓xThe␈α⊂program␈α⊂should␈α⊂be␈α∂robust␈α⊂in␈α⊂the␈α⊂following␈α∂sense.␈α⊂ It␈α⊂should␈α⊂check␈α∂that␈α⊂␈↓↓e␈↓␈α⊂is␈α⊂a␈α∂␈↓¬LAMB␈↓-
␈↓ ↓H␈↓␈↓ ↓xexpression␈αand␈αreturn␈αan␈αappropriate␈αmessage␈αif␈αnot.␈α It␈αshould␈αcheck␈αeach␈αelement␈αof␈α␈↓↓rlist␈↓␈αto
␈↓ ↓H␈↓4␈↓ H


␈↓ ↓H␈↓␈↓ ↓xsee␈α∞that␈α∞it␈α∞denotes␈α∞a␈α∞reduction␈α∞and␈α∞complain␈α
if␈α∞not.␈α∞ Before␈α∞a␈α∞reduction␈α∞is␈α∞applied,␈α∞a␈α
check
␈↓ ↓H␈↓␈↓ ↓xshould be made that is does indeed apply and appropriate complaints made if not.
␈↓ ↓H␈↓Some examples follow.  Let

␈↓ ↓H␈↓        ␈↓↓e=␈↓¬(LAMB 0 (APPL (X . 1) (X . 0)))␈↓↓␈↓
␈↓ ↓H␈↓        ␈↓↓e1=␈↓¬(LAMB 1 (APPL (X . 0) (X . 1)))␈↓↓␈↓
␈↓ ↓H␈↓        ␈↓↓e2=␈↓¬(LAMB 2 (APPL (X . 2) (X . 1)))␈↓↓␈↓
␈↓ ↓H␈↓        ␈↓↓e3=␈↓¬(LAMB 2 (APPL (X . 2) (LAMB 1 (APPL (X . 0) (X . 1)))))␈↓↓␈↓
␈↓ ↓H␈↓        ␈↓↓e4=␈↓¬(APPL (LAMB 1 (LAMB 0 (APPL (X . 1) (X . 0))))␈↓↓␈↓
␈↓ ↓H␈↓                  ␈↓¬(LAMB 1 (APPL (X . 0) (X . 1))))␈↓
␈↓ ↓H␈↓        ␈↓↓rlist=␈↓¬((ALPHA 0 2 NIL) (BETA NIL))␈↓↓␈↓

␈↓ ↓H␈↓then

␈↓ ↓H␈↓        ␈↓↓freefor[e1,␈↓¬1␈↓↓,e]=␈↓¬NIL␈↓↓␈↓
␈↓ ↓H␈↓        ␈↓↓rename[␈↓¬0␈↓↓,␈↓¬2␈↓↓,e]=e2␈↓
␈↓ ↓H␈↓        ␈↓↓freefor[e1,␈↓¬1␈↓↓,e2]=␈↓¬T␈↓↓␈↓
␈↓ ↓H␈↓        ␈↓↓substfree[e1,␈↓¬1␈↓↓,e2]=e3␈↓
␈↓ ↓H␈↓        ␈↓↓LAMB-reduce[e4,rlist]=e3]␈↓

␈↓ ↓H␈↓        After␈α⊃we␈α⊃discuss␈α⊃sequential␈α∩programs␈α⊃and␈α⊃I/O,␈α⊃we␈α∩will␈α⊃see␈α⊃how␈α⊃␈↓↓LAMB-reduce␈↓␈α∩can␈α⊃be
␈↓ ↓H␈↓␈↓ ↓xconverted␈α∞in␈α
to␈α∞an␈α∞interactive␈α
program␈α∞that␈α
you␈α∞can␈α∞have␈α
various␈α∞conversations␈α∞with␈α
about
␈↓ ↓H␈↓␈↓ ↓x␈↓¬LAMB␈↓-expressions.